\section{Sémantické stromy}

Už sme povedali, že Herbrandovské interpretácie sú to pravé orechové,
čo chceme overovať. Ostáva nám ale vyriešiť problém, ako ich nejakým
spôsobom postupne preberať. A práve na to nám budú slúžiť sémantické
stromy.

\begin{definicia}[Kontrárna dvojica]
    Majme nejaký literál (elementárna formulu) $A$. Dvojicu
    $\langle A, \neg A \rangle$ budeme nazývať kontrárnou dvojicou.

    Ak klauzula obsahuje kontrárnu dvojicu, potom je vždy platná a
    teda je to tautológia.
\end{definicia}

\begin{definicia}[Sémantický strom]
    Nech $S$ je množina klauzúl a $A$ je Herbrandovská báza pre
    množinu $S$. Pod sémantickým stromom pre množinu klauzúl $S$
    budeme rozumieť zakorenený dolu rastúci strom
    v ktorom je každej hrane pripísaná množina atómov alebo negácií
    atómov (teda vlastne množina literálov) z Herbrandovskej bázy,
    pričom platí:
    \begin{enumerate}
        \item Z každého vrchola stromu vychádza konečný počet hrán.
            Ooznačme ich ich $l_1, l_2, \dots, l_n$.
            Nech $Q_i$ je konjunkcia všetkých literálov
            pripísaných hrane $l_i$, potom požadujeme aby 
            $Q_1 \lor Q_2 \lor \cdots \lor Q_n$ bola tautológia.

        \item Označme pre vrchov $v$ symbolom $I(v)$
            zjednotenie všetkých množín literálov pripísaných hranám cesty,
            ktorá vedie z koreňa do vrcholu $v$. Potom $I(v)$
            nesmie obsahovať kontrárne dvojice.
    \end{enumerate}
\end{definicia}

\begin{definicia}[Úplný sémantický strom]
    Nech $A=\{ A_1, A_2, \ldots A_n \}$ je Herbrandovská báza pre množinu
    klauzúl $S$.
    Hovoríme, že sémantický strom prislúchajúci $S$ je úplný,
    ak pre každý koncový vrchol(list) $v$ platí:
    $I(v)$ obsahuje $A_i$ alebo\footnote{Toto je exkluzívne alebo. Nemôže
    totiž platiť, že by obsahovala obe formuly} $\neg A_i$ pre každé $i$.
\end{definicia}

\begin{priklad}
    \label{prikl:semantic-tree-example1}
    Uvažujme množinu klauzúl $S = \{P,Q\}$. Potom úplný sémantický strom
    pre túto množinu môže vyzerať napríklad ako na obrázku
    \ref{fig:semantic-tree-example1}.

    \begin{figure}[h]
        \centering
        \includegraphics{img/09stromy/stromy.11.mps}
        \caption{Jeden z možných sémantických stromov pre príklad
                \ref{prikl:semantic-tree-example1}}
        \label{fig:semantic-tree-example1}
    \end{figure}
\end{priklad}

\begin{priklad}
    \label{prikl:semantic-tree-example2}
    K tej istej množine klauzúl môžeme mať viacero sémantických stromov,
    dokonca aj viacero úplných sémantických stromov.
    Uvažujme napríklad množinu klauzúl $S$, ktorá H-bázu $A: \{ P, Q, R \}$.
    Potom 2 úplné sémantické stromy pre túto množinu sú naznačené na
    obrázku
    \ref{fig:semantic-tree-example2}.

    \begin{figure}[h]
        \centering
        \subfigure{
            \includegraphics{img/09stromy/stromy.21.mps}
        }
        \subfigure{
            \includegraphics{img/09stromy/stromy.22.mps}
        }
        \caption{Sémantické stromy pre príklad
                \ref{prikl:semantic-tree-example2}}
        \label{fig:semantic-tree-example2}
    \end{figure}
\end{priklad}


\begin{priklad}
    \label{prikl:semantic-tree-example3}
    Veľmi malý strom môžeme dostať v prípade, ak $S=\{P(x),\ P(a)\}$. Vtedy
    je báza $A:\{P(a)\}$ (nemáme žiadne funkčné symboly a teda si vystačíme
    s konštantou) a strom vyzerá nasledovne (obr.
    \ref{fig:semantic-tree-example3}):

    \begin{figure}[h]
        \centering
        \includegraphics{img/09stromy/stromy.31.mps}
        \caption{Jeden z možných sémantických stromov pre príklad
                \ref{prikl:semantic-tree-example3}}
        \label{fig:semantic-tree-example3}
    \end{figure}
\end{priklad}

\begin{priklad}
    \label{prikl:semantic-tree-example4}
    Sémantický strom zďaleka nemusí byť konečný. Uvažujme napríklad množinu
    klauzúl $S=\{P(x), Q(f(x)) \}$.
    Vtedy je herbrandovská báza nekonečná: 
    $\{ P(a),\ Q(a),\ P(f(a)),\ Q(f(a)),\ \ldots \}$.
    A pretože báza je nekonečná, musí byť nekonečný aj strom, ak chceme aby
    bol úplný. Jeden taký strom je znázornený na obrázku
    \ref{fig:semantic-tree-example4}):

    \begin{figure}[h]
        \centering
        \includegraphics[scale=0.9]{img/09stromy/stromy.41.mps}
        \caption{Nekonečný sémantický strom pre príklad
                \ref{prikl:semantic-tree-example4}}
        \label{fig:semantic-tree-example4}
    \end{figure}
\end{priklad}

\begin{poznamka}
    Radi by sme upozornili na istú drobnosť -- definícia úplného stromu má
    isté problémy v prípade nekonečných stromov, pretože v nich nemáme
    koncové vrcholy. Preto definíciu upravíme nasledovne:
    Strom je úplný ak pre každú (nekonečnú) cestu platí, že obsahuje $A_i$
    pre všetky $i$.
\end{poznamka}

\begin{poznamka}
    \noindent
    \begin{itemize}
    \item Na úplný sémantický strom sa teda môžeme pozerať ako na organizované
        preberanie všetkých možných interpretácii.
    \item Navyše, na množinu $I(v)$ pre vrchol $v$ sa môžeme pozerať ako na
        čiastočnú interpretáciu (interpretuje len niektoré prvky bázy).
    \item Už vieme, že množina klauzúl $S$ je nesplniteľná $\iff$
        je nepravdivá pre všetky herbrandovské interpretácie. Otázka znie,
        ako sa to prejaví na sémantickom strome. Vieme, že každá klauzula
        je konečný objekt. Preto sa musí nájsť nejaká konečná čiastočná
        interpretácia zamietajúca túto klauzulu.

        V prípade, ak množina základných inštancií $I'(v)$ prvkov $I(v)$
        je odmietnutá, na tomto mieste môžeme prehľadávanie stromu ukončiť,
        pretože žiadna interpretácia nevyhovuje. Hovoríme tiež,
        že na tomto mieste môžeme strom \emph{odrezať}.
    \end{itemize}
\end{poznamka}

\begin{definicia}[Odmietajúci vrchol]
    Vrchol $v$ sémantického stromu pre množinu klauzúl $S$ sa
    nazýva odmietajúcim, ak  $I(v)$ odmieta niektorú základú inštanciu
    klauzuly z množiny $S$, no ľubovoľný vrchol $v'$  na ceste z koreňa 
    do vrcholu $v$
    neodmieta žiadnu základnú inštanciu klauzúl z $S$.
\end{definicia}

\begin{definicia}[Uzavretý sémantický strom]
    Hovoríme, že sémantický strom $T$ pre množinu klauzúl $S$
    je uzavretý, ak každá vetva $T$ končí odmietajúcim vrcholom.
\end{definicia}

\begin{definicia}[Akceptujúci vrchol]
    Vrchol $v$ sémantického stromu $T$ pre  množinu klauzúl $S$ 
    nazývame akceptujúcim, ak všetky nasledujúce
    vrcholy vrchola $v$ sú odmietajúce.
\end{definicia}

\begin{priklad}
    \label{prikl:semantic-tree-example5}
    Uvažujme množinu klauzúl
    $S= \{ P,\ Q \lor R,\ \neg P \lor \neg Q,\ \neg R \lor \neg P \}$.
    Herbrandovskú báza je $\{P, Q, R\}$. Na obrázku
    \ref{fig:semantic-tree-example5}.

    \begin{figure}[h]
        \centering
        \subfigure[Pôvodný strom]{
            \includegraphics{img/09stromy/stromy.51.mps}
        }
        \subfigure[Strom vzniknutý odrezaním odmietajúcich vrcholov]{
            \includegraphics{img/09stromy/stromy.52.mps}
        }
        \caption{Odrezanie sémantického stromu z príkladu
                \ref{prikl:semantic-tree-example5}}
        \label{fig:semantic-tree-example5}
    \end{figure}
\end{priklad}



\begin{priklad}
    \label{prikl:semantic-tree-example6}
    Uvažujme množinu klauzúl $S=\{ P(x),\ \neg P(x) \lor Q(f(x)),\ \neg Q(f(x)) \}$.\footnote{
        Na tomto mieste má Toman v poznámkach $P \lor Q(f(x))$ ale na
        prednáške to opravil}
    Herbrandovská báza pre množinu klauzúl $S$ je
    $\{ P(a),\ Q(a),\ P(f(a)),\ Q(f(a)),\ \ldots \}$. Orezaný sémantický
    strom pre túto množinu klauzúl možno nájsť na obrázku
    \ref{fig:semantic-tree-example6}.

    \begin{figure}[h]
        \centering
        \includegraphics{img/09stromy/stromy.61.mps}
        \caption{Odrezaný sémantický strom z príkladu
                \ref{prikl:semantic-tree-example6}}
        \label{fig:semantic-tree-example6}
    \end{figure}
\end{priklad}


